Nuprl Lemma : map-decide
11,40
postcript
pdf
A
,
B
:Type,
b
:(
A
+
B
),
f
,
L1
,
L2
:Top.
map(
f
;case
b
of inl(
a
) =>
L1
(
a
) | inr(
a
) =>
L2
(
a
))
~
case
b
of inl(
a
) => map(
f
;
L1
(
a
)) | inr(
a
) => map(
f
;
L2
(
a
))
latex
Definitions
t
T
,
Top
,
x
:
A
.
B
(
x
)
Lemmas
top
wf
origin
A, B:Type, b:(A + B), f, L1, L2:Top.
A, B:Type, b:(A + B), f, L1, L2:Top.
Tx:A. B(x)